Nuprl Lemma : decidable-exists-finite
0,22
postcript
pdf
T
:Type,
P
:(
T
Prop). (
x
:
T
. Dec(
P
(
x
)))
finite-type(
T
)
Dec(
x
:
T
.
P
(
x
))
latex
Definitions
x
.
t
(
x
)
,
Surj(
A
;
B
;
f
)
,
P
&
Q
,
P
Q
,
A
B
,
,
P
Q
,
{
i
..
j
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
finite-type(
T
)
,
Dec(
P
)
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
Prop
,
t
T
Lemmas
decidable
wf
,
finite-type
wf
,
int
seg
wf
,
decidable
ex
int
seg
,
decidable
functionality
origin
T:Type, P:(T
Prop). (x:T. Dec(P(x))) 
finite-type(T) Dec(
x:T. P(x)) T:Type, P:(TProp). (x:T. Dec(P(x))) finite-type(T) Dec(x:T. P(x)) 
x. t(x)
Q
B
Q
} Qx:A. B(x)x:A. B(x)
T